This invention relates to the automatic generation of vector sequences for the validation of circuit design. In particular, the vector sequences generated are used as inputs to a circuit under simulation to determine whether the desired outputs are produced. More particularly, the invention is embodied in a system, a method, and a program product for the automatic generation of vector sequences for the validation of circuit design, in a manner that targets an observability based coverage metric.
The following papers provide useful background information on the indicated topics, all of which relate to this invention, and are incorporated herein by reference:
A finite state machine (FSM) implementation model:
R. C. Ho, C. H. Yang, M. A. Horowitz, and D. L. Dill, xe2x80x9cArchitecture Validation for Processors,xe2x80x9d in Proceedings of the 22nd Annual Symposium on Computer Architecture, June 1995.
Statement Coverage in HDL Code:
K.-T. Cheng and A. S. Krishnakumar, xe2x80x9cAutomatic Functional Test Generation Using the Extended Finite State Machine Model,xe2x80x9d in Proceedings of the 30th Design Automation Conference, pp. 86-91, June 1993.
Observability-based statement coverage metric:
S. Devadas, A. Ghosh, and K. Keutzer, xe2x80x9cAn Observability-Based Code Coverage Metric for Functional Simulation,xe2x80x9d in Proceedings of the International Conference on Computer-Aided Design, pp. 418-425, November 1996.
Evaluation Procedure for Observability-Based Statement Coverage Metric:
F. Fallah, S. Devadas, and K. Keutzer, xe2x80x9cOCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional Simulation,xe2x80x9d in Proceedings of the 35th Design Automation Conference, pp. 152-157, June 1998.
Recent Algorithms for Solving Hybrid-Satisfiability (HSAT) Problems:
F. Fallah, S. Devadas, and K. Keutzer, xe2x80x9cFunctional Test Generation Using Linear Programming and 3-Satisfiability,xe2x80x9d in Proceedings of the 35th Design Automation Conference, pp. 528-533, June 1998.
Application of SAT Algorithms in CAD:
T. Larrabee, xe2x80x9cTest Pattern Generation Using Boolean Satisfiability,xe2x80x9d IEEE Transactions on Computer-Aided Design, vol. 11, pp. 4-15, January 1992.
Verilog:
D. E. Thomas and P. R. Moorby, The Verilog Hardware Description Language. Kiuwer Academic Publishers, Boston, Mass., second ed., 1994.
Vis verification system:
R. K. Brayton and others, xe2x80x9cVIS: A System for Verification and Synthesis,xe2x80x9d in Proc. Computer-Aided Verification, vol. 1102, pp. 428-432, June 1996.
There will now be provided a discussion of various topics to provide a proper foundation for understanding the invention.
Digital computers have made possible many changes in the scientific, industrial, and commercial arenas. Today, many businesses cannot function without the aid of working information systems. Many special-purpose and general-purpose computers are well-known.
A block diagram of a simple general-purpose digital computer is shown in FIG. 1, although the drawing figure could also pertain equally well to a special-purpose digital computer, depending on the functionality provided. Reference numeral 10 indicates the general-purpose digital computer. Such a computer may include a central processing unit 100, also referred to as a CPU. The main memory 110 may be understood to be a RAM. The computer in this a simplified diagram has only one I/O processor 120. The I/O processor 120 controls I/O devices 130. The I/O devices 130 include a display, a keyboard, a printer, a disk drive, and a mouse. It will be understood that this diagram is for explanatory purposes only, and is not intended in any way to limit the invention.
The CPU 100 includes a control unit, an ALU, and registers. The control unit is responsible for fetching instructions from main memory 110 and determining their type. The ALU performs operations, such as ed. and Boolean AND, needed to carry out the instructions. The registers of the CPU 100 provide a small, high-speed memory used to store temporary results and certain control information. The registers may each be designated a certain function, or may be general-purpose registers. Included in the registers is a program counter PC, which points to the next instruction to be executed. There is also an instruction register IR, which holds the instruction currently being executed.
It will be appreciated that the CPU 100, the main memory 110, and the I/O processor 120 are interconnected by buses. Communications between these different units takes place across the buses.
Thus, it can be seen that a digital computer is an interconnection of digital modules. There are modules within the CPU 100, and be CPU, the main memory 110, and the I/O processor 120 also may be thought of as modules themselves. On a larger scale, when these complements are all included in the same container, this container may be understood to be a module, and the different I/O devices (such as display and keyboard) may be understood to be modules themselves.
The miniaturization of digital computers is a useful and exciting phenomenon. A CPU enclosed in a small integrated circuit package is referred to as a microprocessor. A microprocessor is just one example of the miniaturization of digital components. When a circuit or a combination of related circuits is miniaturized and produced on a single chip, such a chip may be called an integrated circuit.
Special production techniques are required to produce an integrated circuit. Such production techniques add greatly to the cost of the final product.
In view of the expense of producing a microprocessor, is very important to ensure that there are no errors in the design that would render the microprocessor unusable. Modern, high-performance microprocessors are extremely complex, however, and require substantial validation efforts to ensure functional correctness. Modern microprocessors contain many architectural features designed to improve performance, including branch prediction, speculative execution, lockup free caches, dynamic scheduling, superscalar execution, and the like. Such features and complexity to a microprocessor, because they constitute modules within the CPU which interact with each other.
As a matter of economics, the great expense of producing a miniaturized microprocessor and then testing it makes it impractical to verify the design on an actual prototype of the microprocessor. Instead of testing an actual microprocessor produced according to a given design, the design is tested by simulating the operation of the microprocessor on a computer.
To simulate the operation of a physical machine, such as a microprocessor, in a digital computer, it is necessary to represent the functionality of the microprocessor in some manner. One of the ways to represent the functionality of a microprocessor in a form usable by a computer is with the hardware description language HDL. In particular, the desired microprocessor is modeled using HDL. The HDL model describes the interconnections of the arithmetic, logic, and memory modules included in a microprocessor.
An HDL model of a microprocessor is comprised of statements in the hardware description language HDL.
There are computer applications available which will accept, as input, an HDL model of a microprocessor. Based on this input HDL model, the computer application will simulate different aspects of the operation of the microprocessor. The precise aspects of this operation to be simulated may be controlled by the person using the computer application.
It will be appreciated, that the operation of the microprocessor (that is, the microprocessor being simulated) cannot be tested without some inputs being provided to the simulated microprocessor. When the simulated microprocessor is provided with inputs, it will respond in certain predefined ways, providing the design is correct. Such a series of inputs may be referred to as a simulation vector (or, for linguistic convenience, simply as a vector). As used herein, xe2x80x9cvectorxe2x80x9d and xe2x80x9cvector sequencexe2x80x9d will generally be used interchangeably.
Today, the most common approach to checking the correctness of the design is to verify that the description of the design in some hardware description language, such as HDL, provides the proper behavior as elicited by a series of simulation vectors.
Simulation is by far the primary design validation methodology in integrated circuit (IC) design and it is likely to remain so for the foreseeable future, especially in the validation of circuits at the Register Transfer Level (RTL, also referred to as RTL circuits). A reason for this is that the typical RTL circuit is derived from a heterogeneous, ad hoc description of the behavior, i.e. there is no formal model against which to compare the behavior of the RTL. In fact, even if there were such a formal model, today""s available verification tools are generally not robust enough to perform an automatic, formal comparison of the RTL against the behavioral model. That leaves some form of simulation as the only alternative to compare the input/output (I/O) response of the RTL against the desired I/O response represented in the specification.
One way to simulate the I/O response of a circuit is through the use of vectors. As already mentioned, a vector may be understood to be a sequence of inputs. Another way to view a vector is as a sequence of assignments of values to input variables defined in the HDL model of a circuit. When a vector is introduced as an input to a circuit being simulated, the output of the circuit may be observed and compared against the desired output response from the specification. To simulate all the behaviors of a circuit, it is not unusual for many vectors to be used.
FIG. 2 shows a conceptual view of a circuit design to be tested. Reference numeral 20 indicates this circuit which will be simulated on a general purpose or a special-purpose computer, such as that shown in FIG. 1. In FIG. 2, reference numeral 150 indicates the inputs to the circuit. Reference numeral 160 indicates the outputs that the circuit will provide. Reference numeral 170 indicates registers of the circuit. It will be appreciated that each input of the circuit may be represented by a variable within the statements of the HDL code. Similarly, each output of the circuit may also be a variable in a statement of HDL code. The same may be said of the registers.
In the highly schematic representation shown in FIG. 2, intermediate variable assignments are not represented; such intermediate assignments are not visible to the outside world until they show up as an output 160.
It is to be understood that, during the simulation of the circuit shown in FIG. 2, a simulation program is active in the main memory 110 of the general purpose computer 10. The simulation program accesses the HDL code which comprises the HDL model of the circuit. The HDL code may be contained in a file and stored on an I/O device 130 such as a disk drive. The simulation program in the main memory 110 is executed in a well-known fashion by the CPU 100 so as to simulate the operation of the circuit described by the HDL model.
A series of vectors may also be provided in a file stored on a medium such as a disk drive. The simulation program may access the vectors and use them to determine what particular sequence of assignments should be made to the inputs 150 of the circuit 20 being simulated. The results of applying the vectors to the circuit 20 being tested may be written by the simulation program to an output file or the like. Such an output file could include information such as the values appearing at each of the outputs 160 after certain steps or at a given time.
Since the desired functionality of the circuit 20 being simulated is known beforehand, the expected results of operating the circuit vis-a-vis the inputs 150 determined by the series of vectors also are known beforehand. When the simulation results do not match the expected results (and assuming that the expected results are correctly determined by the designer), there is an error in the design.
The foregoing sequence of events is generally shown in FIG. 3, in which reference numeral 180 indicates the HDL code comprising the model of the circuit 20 to be simulated. Reference numeral 190 indicates a file or the like of input vectors which will be used at the inputs 150 of the circuit 20. The HDL code 180 and the input vectors 190 are taken as input by a general purpose or special-purpose computer 10. The computer 10 simulates the functions of the circuit 20 defined by HDL code 180 in response to the input vectors 190 and may produce results 200. The results 200 may be stored in a file, displayed on a display, sent to a printer, etc.
Simulation may be the most time-consuming task in the design of integrated circuits. Simulation time clearly influences the time to market. A major task of simulation is the preparation (or generation) of vectors. Vector generation is typically done manually by verification engineers based on a study of the HDL code 180 that defines the design of a circuit to be simulated. Vector generation time, and the actual simulation time using the vectors, both contribute to the time spent in validating the design. Clearly, there will always be some need for the manual generation of certain simulation vectors to check certain special functions.
To aid in the generation of vectors, various automated approaches have been taken. An automated approach to generating vectors is typically related to a coverage metric. A coverage metric may focus on generating vectors that cover HDL code paths, HDL code lines, transitions of a finite state machine (FSM) model, or the like. The choice of one or more coverage metrics influences the computational requirements of automatic vector generation, and the size of the generated vector set, and ultimately the time it takes to simulate the generated vectors.
In the automatic generation of vectors, one goal is to develop in designers a confidence that the vectors generated using the one or more coverage metrics detect a significant number of errors. By so doing, a reduction could be made in the level of effort directed toward the manual generation of vectors. What is needed is an automatic way to generate the majority of vectors now manually produced by verification engineers. This would result in a significant reduction in design turnaround time.
Since the choice of coverage metrics is so influential in the amount of computational effort expended and the size of the set of vectors, a key issue is what constitutes a reasonable suite of coverage metrics.
In order to detect an error, simulation must visit the site of the error, and subsequently propagate the effect of the error to an observable output.
A coverage metric must begin with some error model and impose observability and controllability constraints on the simulation to be useful. An additional requirement is efficient evaluation of the coverage metric, if it is to be used in the inner loop of vector generation. The complete coverage of all paths in the HDL code 180 or the coverage of all transitions in a finite state machine (FSM) model of the implementation results in too many vectors to be usable. Approaches that generate vectors to cover only selected transitions in the FSM model or only selected paths in the HDL code 180 are much more practical. Coverage of all statements in the HDL code 180 is more tractable than path or transition coverage, but again not very meaningful since it does not address the observability requirement.
Recent useful work has been done in the development of an observability based code coverage metric, as will now be described. For linguistic convenience, the material that follows may be referred to as a first observability based approach. This first observability based approach is reported in an article by S. Devadas, A. Ghosh, and K. Keutzer, xe2x80x9cAn Observability-Based Code Coverage Metric for Functional Simulation,xe2x80x9d in Proceedings of the International Conference on Computer-Aided Design, pp. 418-425, November 1996.
It will be appreciated that, when attempting to make sure that each statement in the HDL model of a circuit is covered by the input vectors, it should be kept in mind that mere coverage is not enough. For example, assume that the input vectors 190 stimulate a bug (i.e., a design error) and that the bug is associated with a certain one of the statements making up the HDL model. It might be the case that the certain statement corresponding to the activated design error assigns the erroneous value to a variable. Subsequently, the variable is provided as one of the two inputs to a Boolean AND operation or the other of the two inputs is always 0. In such a case, even though there is a design flaw, it will be impossible to observe any impact of this error in one of the outputs 160 of the circuit 20.
In other words, the fact that a statement with a bug has been activated by input stimuli does not mean that the observed outputs of the circuit simulated by the simulation program will be incorrect.
The problem of verifying the correctness of an HDL description of circuit behavior is similar to the software testing problem because the description of circuit behavior is similar to a program written in some high-level programming language like C or C++.
To explain certain terms, a discussion of control flowgraphs and path testing will now be provided.
A control flowgraph is a graphical representation of a program""s control structure. A control flowgraph includes processes, decisions, and junctions. A process is a sequence of program statements uninterrupted by either decisions or junctions. A process has one entry and one exit. A decision is a program point at which the control flow can diverge. A junction is a point in the program where the control flow can merge. An example of a control flowgraph for simple program is shown in FIG. 4. A process is shown as a rectangle, a decision is a diamond, and a junction is a circle.
A path in the control flowgraph is a sequence of processes that starts at an entry, junction, or decision and ends at another, or possibly the same junction, decision, or exit.
Given a set of program stimuli, one can determine the statements activated by the stimuli (i.e. vector) by applying the stimuli to the control flowgraph. A line coverage metric measures the number of times every process (and therefore constituent statements) is exercised by the program stimuli. In the case of branch coverage, the number of times each branch is taken under the set of vectors is measured. Path coverage measures the number of times every path in the control flowgraph is exercised by the vectors. The goal of software testing is to have 100% path coverage, which implies branch and line coverage. However, 100% path coverage is a very stringent requirement and the number of paths in a program may be exponentially related to the program size.
Other coverage metrics are also known, for example, multi-condition coverage, loop coverage, and relational operator coverage.
Such coverage metrics require activation but do not relate to the observability conditions required to see the effect of possible errors in the activated statements. For example, in the control flowgraph shown in FIG. 4 an error in the computation of V never propagates to the LOOP if Z is greater than or equal to 0. The path coverage metric will satisfy observability requirements if paths from program inputs to program outputs are exercised and the values of variables are such that the erroneous value is not masked. However, the simple path coverage metric does not explicitly evaluate whether the effect of an error is observable at an output.
In software testing (as opposed to simulating a circuit modeled in HDL code), the problem of observing the effect of an activated and possibly erroneous statement is deferred until test implementation. In test implementation of software, additional testing code is added to points in the program which are hard to force to particular values (i.e., added controllability is provided), and at those points where information is lost (i.e., added observability is provided). One problem with these internal test drivers is that variable values may not be easily translatable into useful data that the programmer can understand and check against the specification.
To model observability requirements, it is necessary to determine whether paths from inputs to outputs are sensitizable, i.e., whether effects of errors can be propagated through paths. To check the sensitizability of a path, tags are used. Tags will be described more below.
Given a set of input vectors to an HDL model, the output response can be determined using a simulator. It is important to note here, that the generation of vectors is not being discussedxe2x80x94only the determination of coverage when the vectors are given. An enhanced simulator can be used to propagate tags from inputs to observable outputs. To deterministically propagate tags through a circuit being simulated, certain assumptions are made. These assumptions do not require assigning particular binary values to the tag, except in the case of tags on single binary variables.
In using tags, it is useful to view a circuit as computing a function, and to view the computation as a series of assignments to variables. Errors in computation are therefore modeled as errors in the assignments, i.e., any value assigned to any variable in the behavioral or RTL description may possibly be in error.
The possibility of an error may be represented by tagging the variable (on the left-hand side of an assignment statement) by a symbol such as xcex94 which signifies a possible change in the value of the variable due to an error. Both positive and negative tags may be considered, with a positive tag written simply as xcex94, and a negative tag written as xe2x88x92xcex94.
Positive and negative tags may be introduced on every assignment statement in the HDL description 180 of a circuit 20. The circuit 20 is simulated for each of the vectors included in the input vectors 190 to determine which of the tags are both activated (by the activation of the corresponding assignment statement) and also propagated to the outputs of the circuit 20. When a tag is propagated to an output, it means that there is a path from the point where the tag was introduced to the output, and that the path was activated by the vector or vectors. During such simulation, the effect of each tag may be separately considered. It is possible, however, to use a simulator to simulate the effects of several tags in parallel as in parallel fault simulation.
The use of tags is an attempt to detect the bugs in the code (i.e., the HDL model) that may result in an incorrect value of some HDL variable. Not all bugs, however, necessarily result in an incorrect value of some HDL variable. Bugs that are errors of omission, or global incorrect assumptions regarding program or algorithm behavior might not cause an incorrect value of an HDL variable. Tags are useful in fulfilling the two basic requirements in verifying an HDL model, namely, activating statements in the code and observing the effect of activation at an output.
For a value at an input 150 to be propagated through a circuit under simulation 20, the other inputs must be at non-controlling values. As mentioned above, if a Boolean AND gate has a 0 input, no value on the other input will propagate to the output since 0 is a controlling value for the Boolean AND gate. In a multiplier, a 0 at one of the inputs will block propagation of any value on the other input.
If there is an error in some assignment, the magnitude of the error determines whether the error will be propagated or not. As an example, consider the following expression:
f=a+b greater than c
In this example, variables a, b, and c are four-bit integers. The vector input to the circuit 20 is represented by:
S=(a=3,b=4,c=5)
A positive error on a (i.e., a+xcex94) is not propagated to f, since the comparison on the right hand side of the assignment statement provides the same value of 1 for f. That is, any positive value for xcex94 will have no effect on the comparison of whether (3+xcex94)+4 is greater than 5. A negative error might be propagated to f resulting in an erroneous value of 0 when the inequality on the right side of the assignment is evaluated. This erroneous value resulting from the comparison on the right side of the assignment will occur if the magnitude of the error is greater than or equal to 2 (i.e., if the negative xcex94 reduces a from its original value of 3 down to 1, making a+b now equal 5, which is not greater than c which has a value of 5).
Thus, the detection of an error in an assignment depends on the magnitude and the sign of the error. Positive and negative tags may be used to model the sign of the errors. However, the magnitude issue results in a dilemma. If a tag has magnitude as a parameter, the number of possible tags is greatly increased. Also, tags having magnitude may be too closely related to particular design errors which may or may not occur.
A useful approach is to make the assumption that the error will be of the right magnitude or magnitudes to propagate through circuit 20. As mentioned above, positive and negative tags model the sign of an error in relation to the value of a variable. In the observability based coverage metric, it may be assumed that the tag introduced in an assignment statement (i.e., the change in the value of the variable on the left-hand side of the assignment) corresponds to an error of appropriate magnitude such that it will propagate through any module provided (a) it is of the appropriate sign and (b) the other inputs to the module are non-controlling (i.e., they do not block propagation).
Functional simulation and statement coverage will now be discussed. Again, it is important to keep in mind that the present discussion relates to a way of determining how many HDL statements are covered, given a known set of input vectors, under an observability based coverage metric.
Tag simulation may be carried out on a given HDL circuit description in exactly the same manner as functional simulation. A functional simulator such as the VERILOG simulator executes initialization statements, and propagates values from the inputs of a circuit to the outputs. It keeps track of time, causing the change to values to appear at specified times in the future. When the simulator has no further statements to execute at any given time instant, it finds the next time-ordered event from the event queue, updates time to that of the event, and executes the event. This simulation loop continues until there are no more events to be simulated or the user terminates the simulation.
Some functional simulators have features that allow the user to determine the execution counts of every module/statement in the HDL description, when the description is simulated with a functional vector set. This allows the user to detect possibly unreachable statements and redundant conditional clauses. The tag simulation method augments this coverage.
The HDL circuit description is pre-processed to extract a flowgraph of the circuit. The flowgraph shown in FIG. 4 does not model concurrency; the HDL model may have interacting concurrent processes. A fork may be added to the flowgraph to allow the modeling of parallelism. An example of a flowgraph with fork nodes is shown in FIG. 5.
It will be appreciated that the flowgraph is not used to perform simulation. Rather, it is used in determining whether a tag can be propagated to an output 160.
In the observability-based coverage metric, assignment statements consisting of arithmetic operations, Boolean word operations, and Boolean operations are considered. Positive and negative tags are injected at every assignment statement and attached to the variables on the left-hand side of the assignment.
If a variable is a collection of bits, it is treated as a single entity. However, if the variable is defined as a collection of bits, but individual ones of those bits are sometimes manipulated, the individual bits are treated as Boolean variables throughout. An IF statement has a control condition which is a Boolean variable. If this Boolean variable is computed, i.e., it is not a primary input, it appears as the left-hand side of some assignment. The tag that is injected for that assignment models errors in the control flow. In such a situation, errors might result in the THEN branch being taken rather than the ELSE branch, or vice versa. No tags are injected for control constructs, though tags must be propagated based on the control flow.
Every assignment statement executed during simulation of functional vectors is also xe2x80x9ctag simulatedxe2x80x9d to determine which tags are propagated. Tags attached to variables on the right hand side of the assignment are propagated and attached to the left-hand side according to a tag calculus used in the observability-based coverage metric.
In the case of strictly Boolean variables, this calculus is equivalent to the D-calculus. For ease of exposition, the propagation of a single tag during simulation will be discussed. In actual implementation, several tags may be injected and propagated in parallel.
First, the tag calculus for Boolean logic gates will be discussed. The calculus for a two-input AND gate and an inverter are shown in the following table.
The four possible values at each input are {0, 1, 0+xcex94, 1xe2x88x92xcex94}. Note that 0xe2x88x92xcex94 is treated similar to 0, and 1+xcex94 is treated much like 1. The entries in the table are self-explanatory. Using this calculus, any collection of Boolean gates comprising a combination logic module can be tag simulated.
Tag propagation through arithmetic operators will now be discussed. This discussion will also include Boolean word operators.
All modules in the circuit being simulated are assumed to be n bits wide. In the following equation, v(f) is a variable on the left side of an assignment statement, and v(a) and v(b) are variables on the right side of an assignment statement. The two variables on the right side of the assignment statement are separated by at least one operator op. For each operator op, after the simulator computes v(f)=v(a)(op)v(b), the variable on the left-hand side of the assignment statement (i.e., v(f), is tagged with a positive or negative xcex94. The tag variable may be written as:
v(f)+xcex94 or v(f)xe2x88x92xcex94
First, an adder module is considered. If all tags on the adder inputs are positive, and if the value v(f) less than MAXINT, the adder output is assigned v(f)+xcex94. It should be noted that MAXINT is the maximum value possible for f. Similarly, if all tags are negative, the adder output is assigned v(f)xe2x88x92xcex94. If both positive and negative tags exist at the inputs of an adder, the output is assumed to be tag-free.
Next, a multiplier module is considered. All tags have to be of the same sign for propagation. A positive xcex94 on input a is propagated to the output f provided v(b)xe2x89xa00 or if b has a positive xcex94. In such a case, the multiplier output is assigned v(f)+xcex94. Likewise, a negative xcex94 on input a is propagated to the output f provided that v(b)xe2x89xa00 or b has a negative xcex94. In such a case, the multiplier output is assigned v(f)xe2x88x92xcex94.
Next, the greater-than (i.e., xe2x80x9c greater than xe2x80x9d) comparator will be discussed. If tags exist on inputs a and b, they have to be of opposite signs, else the tag is not propagated to the output. Assume a positive tag on a alone, or a positive tag on a and a negative tag on b. If v(a)xe2x89xa6v(b) then the tag (or tags) gets propagated to the output. Otherwise, no tag propagation occurs. The comparator output is assigned 0+xcex94. Other tags and other kinds of comparators are handled similarly.
For a bitwise AND, all tags have to be of the same sign for propagation to occur. Given a positive tag on a and a tag-free b, if at least one of the bits in b is not 0, and v(a)xe2x89xa02nxe2x88x921 and v(b)xe2x89xa02nxe2x88x921, then v(f)=v(a) and v(b) is computed and assigned the output v(f)+xcex94. Negative tags are handled in a similar fashion.
For a bitwise NOT: v(f)i={overscore (v(ai))} where 0xe2x89xa6i less than n. For a positive tag on a, the output is assigned v(f)xe2x88x92xcex94.
Propagation through IF statements requires pre-processing the program. The reachability of processes from decisions (IF statements) in the control flowgraph is determined. Since each process has a single entry and a single exit, all the statements within each process will have the same reachability properties.
It is assumed, without loss of generality, that each decision is binary. For each decision, the set of all processes that can be reached when the control condition c is true, namely Pc, is determined, and also the set that can be reached if the control condition is false, namely P{overscore (c)}.
When an IF statement is encountered by the simulator, there are two cases:
1. There is no tag in the control condition. In this case simulation proceeds normally. In the appropriate processes, statements are executed and tags (if any) are propagated/injected.
2. If a tag is attached to the control condition c (which is a Boolean variable), it means that the tag will result in the incorrect branch being taken. Assume a positive tag on c (i.e., c+xcex94). If the value of c on the applied vector is 1, the tag is not propagated. However, if the value of c is 0, then all the assigned variables in the processes P{overscore (c)}xe2x88x92Pc are tagged. Under the tag condition these assignments will be missed, and hence the output variables are tagged. A positive tag is applied if the new value (after assignment) is less than the old value, a negative tag if the new value is greater than the old value, and no tag if both values are equal or if the old value is undefined. This assumes that equivalent statements in both clauses have been extracted out of the IF (placed before the decision). It should be noted that tags could also have been assigned to variables in Pcxe2x88x92P{overscore (c)}, because under the tag condition these assignments are wrongly made, but doing so would require multiple trajectory simulation which may be too expensive.
For each functional vector, or functional vector sequence, for every positive or negative tag injected on each assigned variable, the calculus just described in the previous section may be used to determine which of the tags is propagated to the output""s of the circuit being simulated 20. The coverage for the functional vector set may be computed as the percentage of tags propagated to the outputs divided by the total number of tags.
Simulation proceeds on the HDL simulation model in an event-driven manner as already described. For each functional vector sequence, though the effect of each tag is considered separately, a parallel tag simulation may be performed or the propagation of multiple independent tags is determined. After each assignment statement is evaluated, it is determined whether the tags on the variables on the right hand side of the statements are propagated to the variable on the left-hand side. Tags are also injected for the assignment on the variable on the left-hand side. Some tags may not be activated by the functional test sequence if the statements in which the tag occurs is not reached.
After each vector in the sequence is simulated, the observable outputs of the HDL model are inspected to determine the tags propagated to the outputs. In the case of sequential machines, tags may propagate to the output only after multiple vectors have been applied.
In many cases a designer may be interested in exercising particular sequences of statements in the HDL model, and observing the effect at the output. Alternately, a designer may be interested in exercising particular modules in the given order and checking the output response. The tag simulation algorithm just mentioned can be extended to keep track of the subpath or subpaths that are activated in propagating the tag to the output. Information regarding the activated paths can be passed along with the coverage numbers.
The first observability based approach having been explained, the discussion will now turn to a second observability based approach which may understood to be an improvement upon the first, in certain respects. This second observability based approach is reported in an article by F. Fallah, S. Devadas, and K. Keutzer, xe2x80x9cOCCOM: Efficient Computationa of Observability-Based Code Coverage Metrics for Functional Simulation,xe2x80x9d in Proceedings of the 35th Design Automation Conference, pp. 152-157, June 1998.
Under the second observability based approach, there is not only the above-identified effective observability-based statement coverage metric in its general sense, but also a fast companion procedure for evaluating it. Again, it is important to note that this second observability based approach is an approach to computing the coverage that is provided by a predetermined set of vectors, where coverage is evaluated based on an observability based metric.
The evaluation procedure is computationally very efficient, more so than the first approach.
In general, the improved evaluation procedure involves breaking up a computation into two phases: functional simulation of a modified HDL model, followed by analysis of a flowgraph extracted from the HDL model. Commercial HDL simulators can be directly used for the time-consuming first phase, and the second phase can be performed efficiently using concurrent evaluation techniques.
Phase 1, more particularly, involves an automatic modification of the given HDL model 180, adding new variables and moving statements out of conditionals, and simulating the given vectors using commercial HDL simulators. Thus, available simulation technology can directly be exploited. There is a loss of simulation efficiency due to the addition of new variables, but this is not very large. The modifications to the HDL model are necessary because of conditionals in the HDL model. Simulating the modified HDL model provides more information than simulating only the original model. This extra information is used in the second phase to perform tag propagation. Tags do not play a part in this first phase.
The simulation of the vectors is necessary also because the vectors are given. The intermediate values cannot be known until the vectors are simulated on the HDL model.
For phase 2, tag injection is performed and propagation is determined. A flowgraph is created from the modified HDL model, and the results of the simulation are used to determine coverage under the observability based criteria. Tag injection simply corresponds to introducing a tag on an edge in the graph (i.e., the flowgraph) and tag propagation corresponds to selectively cursing paths from the age to the output nodes. The efficiency in this phase comes from using concurrent evaluation techniques. The tag simulation calculus described above is not used in phase 1, but only in phase 2. Nevertheless, understanding the tag simulation calculus helps to understand why the modifications to the HDL are performed in this evaluation procedure.
Under the evaluation procedure being described, there is an automatic modification of the HDL model such that the HDL simulation produces enough information to compute coverage during phase 2. The modification is illustrated for several commonly occurring cases below. The modifications all require the addition of new variables.
A simple conditional will first be used as an example to show how the HDL code 180 is modified. The following code represents the original HDL:
The modification to the original HDL code 180 results in the following:
Consider the case of a tag on cexp (cexp may be understood to mean a conditional expression). During the simulation of the modified code, the values of both expr1 and expr2 are computed, and stored in the new variables x1 and x2. The old value of x is known, and the new values of x corresponding to the execution of both the THEN and ELSE clauses, regardless of the value of cexp. This will allow the correct propagation of positive or negative tags on cexp in phase 2.
Nested conditionals will now be considered. The case of nested conditionals is more complicated. Further, the situation where variables such as x are assigned values that depend on the old values (e.g., increment operation) must be considered. The original code is as follows:
The transformed code, which will compute the necessary information to perform propagation of tags on cexp1 or cexp2 is as follows:
The case of a simple loop will now be considered. The interesting case is where there is a tag on the variable N. The following is the original HDL code 180 including a simple loop:
The transformed code is as follows:
If there is a negative tag on N, then that corresponds to the situation that the loop is iterated fewer than N times. If there is a positive tag on N, then that corresponds to the situation or the loop is iterated more than N times. To minimize simulation overhead, exactly one more iteration of the loop is performed. Given the extra conditional in the modified loop, the two pieces of code result in the same value for x. However, x1 will contain the value for the case where the loop is iterated N+1 times.
Similar transformations can be made for WHILE and REPEAT loops.
Tags are not injected on the loop counter variable i. It is assumed that errors on i are reflected by changes in the number of loop iterations, i.e., N. Propagating tags on variables such as x does not require additional information.
Now the case of a conditional with an event will be considered. Events in Verilog correspond to setting variables that affect other processes. Consider the following original HDL code 180:
The following is the transformed HDL code 180:
This case is similar to the simple conditional case, where the concern is with a tag on cexp. The additional complication is the event ec1. The event should not be moved outside the THEN clause, because there is no way of undoing the effect of the event in the simulator, if the clause is not going to be executed.
Finally, a loop and a conditional will be considered. A loop inside a conditional is handled like any other statement. A conditional inside a loop requires a more complicated transformation. This is the original HDL code 180:
The transformed HDL code 180 is as follows:
It is desired to propagate tags on both iteration count variable N, and the conditional expression cexp in phase 2. The code needs to be transformed such that there is enough information to propagate either tag.
Consider a tag on N, and no tag on cexp. This is similar to the simple loop case, except that values are being computed in both clauses of the conditional. The case of no tag on N and a tag on cexp is the same as the simple conditional case.
In a single tag model, it may be the case that a tag injected on a variable y is propagated to both N and cexp.
Given the information regarding variable values for the simulated functional vectors, it will now be described the manner in which concurrent tag propagation is performed. A flowgraph data structure that enables efficient tag propagation is used. Similarities between this second observability based approach and the first observability based approach described above will be noticed.
A graph is created from the HDL model. The graph may be represented as G(V,E,L(E)). Here, V indicates the set of all vertices, E indicates the set of voltages, and L(E) represents the labels of the edges of the flowgraph. Each vertex vxcex5V corresponds to a variable in the HDL model. Each edge e(v,w)xcex5E is a directed edge from source node v to destination node w. The edge implies a data dependence between the nodes. In other words, it may be said that node w depends on v.
The label of an edge l(e)xcex5L contains the information below:
Line number: the edge exists because of a data dependence. A particular line of the modified HDL file containing the description of the model is associated with the edge. For example, given a=b+c in a particular Line 154, the edges from b to a and c to a will both have Line 154 as a label.
Conditional expression: in order for a data dependency to exist, there is a conditional expression attest to be true. For example, given
the conditional expression for the edge from b to a would be x greater than y. Since the nested conditionals have been removed from the modified HDL model, there is no need to conjunct multiple expressions. The expression will correspond to the conditional clause of a single IF statement in the original HDL model.
Indices for array variables: Arrays are common in HDL models. There will be a separate tag associated with each array element, resulting in an array of tags. Given:
a[i]=b[i+4];
there will be a single node for the array b and the array a, and an edge from b to a. Information corresponding to the array indices will be associated with the edge from b to a. In general, two indices are required, one for b and one for a. It is necessary to compute these indices dynamically during tag propagation.
Type of dependence: Dependence can be, normal, conditional, through task or function call, and through module instantiation. For example, given:
there is an edge from x to a and from y to a. These edges are conditional edges. The edges from b and c to a are normal edges. A task or function call dependency is a dependency between inputs and outputs of a task enable or function call. If there is a tag on one of the inputs, or the tag-injected line is inside the task or function, there may be tags propagated to the output of the task or function.
Propagation multiplier: a multiplier is associated with each edge that will be used to multiply tags propagating down the edge. These multipliers may be expressions. For example, given a=bxe2x88x92c, the edge between b and a has a +1 multiplier, but the edge from c to a has a xe2x88x921 multiplier. (This is because a positive tag on c should result in a negative tag on a). There is an additional complication for ages whose dependence type is conditional. Consider the following:
In this case, the conditional dependence edge from x to a will have the expression a1xe2x88x92a2 as the propagation multiplier. Of interest is only the sign of a1xe2x88x92a2, not its magnitude.
A single observable vertex 0 is created in the graph, and does not correspond to any variable. The variables in each xe2x80x9cdisplayxe2x80x9d or xe2x80x9cmonitorxe2x80x9d statement in the HDL model will be connected to 0 via edges. Each edge will have a Line number corresponding to the display statement. The conditional expression will always be true, and the propagation multiplier will be +1 or xe2x88x921. If array variables are displayed, the index of the variable will be attached as a label for the edge.
Concurrent tag propagation under the second observability based approach will now be described.
Tag propagation is performed on the graph structure, and uses information obtained from the simulation trace of the modified HDL model. For each vector, all tags they can be propagated to the observable vertex 0 are determined using con current tag propagation. The steps are:
1. Each edge in the graph is first determined to be active or inactive for the given vector. An active edge is an edge that can propagate a tag from a predecessor node to the successor node. Whether an edge is active or not depends on the tag simulation calculus described above. For example, given the statement C=Axc3x97B, if B is 0, then the edge from A to C will be inactive. A complication is that edges corresponding to the control statements may be active or inactive depending on the sign of the tag which is propagated, as well as the value of the control predicate under the given vector. For example, in:
there is an edge with conditional dependence from y to x. This edge is inactive if exp1xe2x88x92exp2=0 for the given vector, and is marked active otherwise. The propagation multiplier of the edge is +1 if expr1xe2x88x92expr2 greater than 0, and xe2x88x921 if expr1xe2x88x92expr2 less than 0. If y=1, then a positive tag on y cannot be propagated to x from y, but a negative tag can.
2. All inactive edges in the graph are deleted.
3. A positive and a negative tag are injected on the observable vertex 0.
4. Starting from the observable vertex 0, and assuming positive (negative) tags on the vertex, edges in the graph are traversed backwards, in the reverse order of simulation trace, determining all nodes nxcex5V that can reach the observable vertex. The vertex 0 is reachable from node n, if, before traversing any of n""s fanin edges, all traversed paths from n to 0 have propagation multipliers of the same sign (the propagation multiplier of a path is simply the product of the propagation multipliers of the constituent edges). Note that paths with multipliers of different signs might result in tag cancellation, and under this second observability based approach it is assumed that the tag is not propagated.
5. Line numbers of edges encountered during the backward traverse determine the tags which are observable in vertex 0.
In the above identified second observability based approach, there is provided and efficient method to compute the coverage under an observability based code coverage metric for a given set of vectors on complex HDL designs. This method offers a more accurate assessment of design verification coverage than line coverage. This second observability based approach also is more computationally efficient than the first observability based approach because it breaks up the computation into two phases: functional simulation of the vectors on a modified HDL model, followed by analysis of a flowgraph extracted from the HDL model. Under this approach, commercial HDL simulators can be directly used for the time-consuming simulation of the first phase, and the second phase can be performed efficiently using concurrent evaluation techniques.
For the sake of background, a discussion will now be presented relating to an approach to generating vectors, namely, vectors designed to exercise selected paths in an HDL model. It should be noted that this vector generation technique does not target an observability based metric, but, rather, is target to path coverage. This path coverage approach is reported in an article by F. Fallah, S. Devadas, and K. Keutzer, xe2x80x9cFunctional Test Generation Using Linear Programming and 3-Satisfiability,xe2x80x9d in Proceedings of the 35th Design Automation Conference, pp. 528-533, June 1998.
This particular path coverage approach provides an example of a recent algorithm for solving hybrid-satisfiability (HSAT) problems.
Under this path coverage approach, selected paths in the HDL model are exercised. The HDL model, as already mentioned, describes the interconnections of arithmetic, logic, and memory modules. Given a path in the HDL model, the search for input stimuli that exercise the path can be converted into a standard satisfiability checking problem by expanding the arithmetic modules into logic gates. Expanding all the arithmetic modules into logic gates, however, is not very efficient.
Here, satisfiability checking is performed directly on the HDL model without converting the arithmetic modules into logic gates. The primary feature of this approach is a seamless integration of linear programming techniques for feasibility checking of arithmetic equations that govern the behavior of data path modules, and 3-SAT checking for logic equations that govern the behavior of control modules. This feature is important to efficiency, since it avoids module expansion and allows work to be done with logic and arithmetic equations whose cardinality tracks the size of the HDL model.
No attempt is made to exercise every path of the HDL model. Rather, the approach is useful with respect to. selective path coverage as a metric for functional vector generation.
It should be noted that there is a public domain 3-SAT based test pattern generator available which includes many different heuristics for fast 3-SAT checking. This path coverage approach augments the 3-SAT framework, and uses a commercial linear programming (LP) solver to implement the algorithm.
The functional vector generation strategy for the path coverage based approach will now be described. Given an HDL model, the strategy involves setting up search problems given the path coverage metric, and solving the search problems to obtain input stimuli. Under this approach, an HDL model is viewed as a structural interconnection of modules. The modules can be comprised of combinational logic, and registers. The combinational logic can correspond to Boolean operators (e.g., AND, OR), or arithmetic operators (e.g., +,  greater than ).
In connection with this explanation, there is provided an example of a module-level sequential circuit corresponding to a greatest common divisor (GCD) circuit, shown in FIG. 6.
Path testing will now be discussed, and first with a focus on combinational circuits. This strategy of generating functional vectors is to sensitize paths from the circuit inputs to circuit outputs. The sensitization of a path can mean many things, and it is more clearly defined below. In general, sensitizing a path implies that the value at the inputs to the path should affect the value at the output of the path. An important point to note is that buses and word-level variables are not expanded into bit-level variables. Therefore, a path can be a collection of electrically distinct signals.
Since there may be exponentially many paths in an HDL model, a subset is used. This subset is chosen such that at least one path in the subset passes through each module input to each module output. That is, if there is a module with two inputs A and B, and two outputs C and C, paths are chosen that pass through Axe2x86x92C, Axe2x86x92D, Bxe2x86x92C, and Bxe2x86x92D.
There are other criteria in choosing paths, and the quality of the generated vector set is dependent on these criteria. In this example, full statement coverage in the HDL model is targeted, and this can be achieved by sensitizing a set of paths that cover each module-input/module-output sub path. Path sensitization will now be discussed in more detail.
A path may be understood to be a set of alternating modules and signals, and may be represented by P={s1, m1, s2, m2, . . . , sn}. The first signal, s1, is a circuit input, and the last, sn, is a circuit output. For each i, the si is an input to module mi and si+1 is an output of module mi. Sensitizing a path simply corresponds to sensitizing each module mi.
A sub path through a module mi, may be understood to be from si to mi and on to si+1. Sensitization of a sub path through a module will require values at the module side-inputs, i.e., the inputs other than si to mi.
For logic gates, the following may be said:
INVERT: no values required.
AND: require side-inputs to be at 1.
OR: require side-inputs to be at 0.
The foregoing rules can be used to determine sensitization for arbitrary collections of logic gates, as well as logic macros such as multiplexers and decoders.
For word-level operators, sensitization needs to be defined on the basis of the logic function of the operator. Arithmetic operators are easy to sensitize; it is necessary merely to check for overflow or underflow. Assuming, for the moment, that it is desired to sensitize the path from A to the module output. Sensitization should reflect the condition that a large enough change in the value of A should result in a change in the module output.
Adder A+B: if there is no concern with overflow, there is no requirement; if there is a concern with overflow, then it is required that A+B less than MAX, where MAX is the largest represented number.
Increment A+k: to avoid overflow A less than MAXxe2x88x92k.
Subtractor Axe2x88x92B: similar to an adder, except the concern relates to underflow.
Comparator A greater than B: it is required that B less than MAX. For other types of comparators, a similar requirement is used.
Scalar multiplication A*k:   A   less than       MAX    k  
xe2x80x83to avoid overflow.
While the above sensitization requirements for logic gates and word level arithmetic operators may appear simple, it should be noted that requirements on intermediate signals in the circuit are sought. Therefore, a Boolean signal c may be requested to be a 1, which is the output of a comparator A greater than B, where A=C+D. (C and D may be circuit inputs or intermediate signals themselves.)
Here, the method of finding input values that sensitize paths is to:
1. Write sensitization requirements on (intermediate) signal values as described above.
2. Write module-inputs module-output relationships for every module in the circuit.
3. Solve a satisfiability problem that corresponds to 1 and 2 above. This produces an input assignment that satisfies the sensitization requirements and is consistent with the behavior of the logic circuit.
Different sensitization criteria could be used without changing the overall framework just described.
So far, only combinational HDL models have been discussed with respect to the path coverage based approach under consideration. In general, HDL models will be sequential, such as the one in FIG. 6, where registers are intermixed with Boolean and arithmetic operators. The approach to handling sequential circuits is to use the conventional time-frame expansion strategy of sequential test generation (this may be understood to be xe2x80x9cunrolling the circuitxe2x80x9d).
A path may be selected from circuit inputs/register outputs to circuit outputs/register inputs. Once the satisfiability problem for path sensitization is set up and solved, it will be required that the circuit inputs be at particular values, and particular values may be required at the register outputs as well. It may be that certain circuit inputs and register outputs can be left undefined.
The required values at the register outputs next need to be justified. This is done using the time-frame expansion strategy. The initial values of the registers are checked. If the initial values are consistent with the required values, there is no need for justification. Otherwise, an attempt is made to determine circuit input values that produce the required values at the register inputs, so, in the next cycle, the register outputs have the correct values. This is done by solving a new satisfiability problem. If no satisfying assignment can be found, the circuit is time-frame expanded over 2 cycles, and an attempt is made to find a sequence of input values of links 2 that produces the required values at the register inputs, solving a larger satisfiability problem. This process may continue until a user-defined limit on the number of time-frames is reached.
In this path coverage or approach being discussed, there is no attempt to propagate values at register inputs to circuit outputs. This approach assumes that all registers are observable during functional simulation.
As was described above, to generate vectors that sensitize a single path, it is necessary to solve several satisfiability problems for a sequential HDL model. Further, the satisfiability problems encountered in the justification (and propagation) steps may result from a time-frame expanded circuit, which is larger than the original, since combinational logic is replicated. Thus, it is very important that the satisfiability algorithm be as powerful as possible. The algorithm provided under this approach will now be discussed.
This algorithm may be referred to as a hybrid algorithm. This algorithm seamlessly integrates linear programming feasibility and 3-satisfiability checking. It is the correlation between word-level variables and Boolean variables that makes this complex. In general, a word level variable A may appear in an arithmetic operation (e.g., C=A+B), and eight bits-masked version may appear in a Boolean operation (e.g., d=anxe2x88x921vb0, where V denotes logical OR).
The 3-Satisfiability (3-SAT) approach was pioneered for use in conjunction with stuck-at fault test generation. Here, however, stuck-at fault testing is not of interest; rather, the interest is in justifying values on a collection of signals. That is, given a logic circuit, it is desired to find an input assignment that produces appropriate signal values at circuit outputs, or intermediate signals. The 3-SAT approach converts this problem into one of satisfying a conjunctive normal form (CNF) expression. Each of the clauses in the CNF have that most 3 variables in them, hence the name 3-SAT.
Consider the circuit of FIG. 7. Assume it is desired to find an input assignment that sets the output to a 1. Clauses for each gate in the circuit are written. These clauses model the input-output relationship for each gate, and are shown below:
({overscore (X)}{overscore (Y)})xc2x7(XY)xc2x7({overscore (Z)}X)xc2x7({overscore (Z)}Y)xc2x7({overscore (X)}{overscore (Y)}Z)
In order to produce a 1 at the output of the circuit, the CNF above needs to be satisfied with Z set to 1. This simplifies to:
({overscore (X)}{overscore (Y)})xc2x7(XY)xc2x7(X)xc2x7(Y)
which is clearly not satisfiable.
The algorithm for satisfiability under this path coverage based approach will now be discussed in more detail. It is assumed that there is given an arbitrary interconnection of combinational modules which include Boolean and word-level operators:
AND, OR, and NOT gates;
Comparison:  greater than ,  greater than =,  less than ,  less than =;
Addition/subtraction: +, xe2x88x92;
Increment/decrement: +/xe2x88x92k;
Scalar multiplication: *k;
Left and right shift:  less than  less than k;  greater than  greater than k.
Any other word-level or Boolean operator that is not one of those listed above is converted into a collection of the listed word-level and Boolean operators. The word-level operators are all linear.
There is given the required said the values for an arbitrary subset of module outputs, and there may be given additional constraints as described above. The task is to find an input assignment that produces the required output values, or to prove that no such assignment exists. This is called the HSAT problem.
There are two kinds of variables, Boolean variables and word-level variables or integers. The word-level operators operate on word-level variables, or as the Boolean operators work on Boolean (single-bits) variables.
It is possible that Boolean operators are applied to word-level variables. For example, a word-level variable A may be operated upon as A+B, and also as A and C, where and corresponds to a bitwise Boolean AND. To represent the bitwise AND operator O(n) Boolean clauses are written over the bits in A and C, namely, anxe2x88x921, anxe2x88x922, . . . , a0, and cnxe2x88x921, cnxe2x88x922, . . . , c0. Here anxe2x88x921 is the most significant bit in A, and a0 is the least significant bit.
The word-level variable A will be used in a linear arithmetic constraint (LAC) to model the word-level operations on A. The correlation/equivalents between A and ai will be xe2x80x9crememberedxe2x80x9d, but represented separately throughout the algorithm.
The range of a variable is the set of values that the variable can take. For example, an integer variable A may take on the values xe2x88x9215 to +15. The Boolean variable ai can only take on the values {0, 1}.
Given the set of combinational modules listed above, for each module there will be written a set of Boolean clauses defining the relationship between the inputs in the outputs of that module. Below, there follows a description of the clauses for Boolean operators, and linear constraints for word-level operators, respectively.
Boolean clauses for Boolean operators are discussed first, and briefly. Clauses (2-SAT and 3-SAT) for each logical gate are written as already described above, for example,
z=AND(x,y): ({overscore (z)}x)xc2x7({overscore (z)}y)xc2x7({overscore (x)}{overscore (y)}z)
Linear constraints are written for each of the word-level operators:
C=A+B: A+Bxe2x88x92C less than =0 and A+Bxe2x88x92C greater than =0
C=A+k: Cxe2x88x92A less than =k and Cxe2x88x92A greater than =k
For scalar multiplication, the constraints may be written as:
C=A*k: Cxe2x88x92kA less than =0 and Cxe2x88x92kA greater than =0
The shift operators  less than  less than  and  greater than  greater than  can be viewed as scalar multiplication. In the case of shifting in 1""s, it may be necessary to add a constant to the above equations. Cyclic shifts may also be modeled, by adding the most significant bit anxe2x88x921 to the equations.
Now a situation in which word-level variables and Boolean operators are correlated will be considered. Consider c=A greater than B. Note that c is a Boolean variable. In the sequel, U refers to 2n, where n is the maximum number of bits in A or B. The constraint is written:
Axe2x88x92B+U(1xe2x88x92c) greater than =1.
In the above equation, if c is 1, then the constraint becomes Axe2x88x92B greater than =1, i.e., A greater than B. If c is 0, then it becomes Axe2x88x92B greater than =1xe2x88x92U, which is always true, given that U is large enough. The constraint is also written:
Axe2x88x92Bxe2x88x92Uc less than =0.
If c is 0, then the constraint becomes Axe2x88x92B less than =0. If c is 1, then the constraint is Axe2x88x92B less than =U, which is always true.
Thus, the two constraints above will express the input-output relationships of a  greater than  comparator. Similar pairs of constraints can be written for the other comparators.
Nonlinear operators such as integer multiplication can be decomposed into linear operators.
Given an arbitrary set of modules, there are three types of constraints: 2-SAT clauses, 3-SAT clauses, and linear arithmetic constraints (LAC). The 2-SAT and 3-US sat clauses are over the Boolean variables. The LAC are over the word-level variables, and some Boolean variables. It thus may be said that:
HSAT=2-SAT+3-SAT+LAC.
These interacting Boolean and linear arithmetic constraints may thus be said to be a system of interacting Boolean and linear arithmetic constraints. The transformation that allows the integration of linear arithmetic constraints and Boolean clauses in this A satisfiability algorithm will now be described.
Note that there is correspondence or correlation between the word-level variables and Boolean variables. For example, the word level variable A may appear in a LAC, and ai, a bit in A, appearing in a 2-SAT clause. It is necessary to ensure that values of word-level variables in the LAC""s are consistent with the values of constituent bits in the Boolean clauses.
Initially, all the variables are unbound or sets to unknown values. During the satisfiability search, which will be described below, Boolean variables or word-level variables may be set. However, if a word-level variable W is correlated to a Boolean variable wi, only the Boolean variable is set to {0, 1}, and the LAC""s that contain W will be transformed. The transformation will now be described.
Assume that 0xe2x89xa6Wxe2x89xa62nxe2x88x921, i.e., W is a positive integer n bits wide. Suppose that w0 is set to 1 in W. Then, there is introduced a new variable, such as V, and instead of W the following is written: 2V+1. The range of V is smaller than that of W, and it is 2nxe2x88x921xe2x88x921. In general, given a word-level variable W, and an arbitrary number of Boolean variables (bits) in W set to 1 or 0, a linear expression can always be written for the arithmetic value for W using:
w=2nxe2x88x921wnxe2x88x921+2nxe2x88x922wnxe2x88x922+ . . . +2w1+w0
If W is of n bits, and r bits are set in W, then, in the worst-case, this will require r+1 new word-level variables, assuming none of the r bits is adjacent. As an example, consider a four-bit W, with w2 set. It may be transformed to 8X+4+y, where xxe2x89xa61, yxe2x89xa63. X is effectively a Boolean variable, and Y is a two-bit integer. W is no longer needed, so the increase in the number of variables is at most r.
For signs/magnitude or two""s complement integers, the appropriate equation is used that corresponds to the arithmetic value of the integer based on the individual bits. For example, the two""s complement equation for an n+1-bit number W, whose most significant bit is the sign bit, would be:
w=xe2x88x922nwn+2nxe2x88x921wnxe2x88x921+2nxe2x88x922wnxe2x88x922+ . . . +2w1+w0
Thus, given an arbitrary setting of Boolean variables that correlates to word-level variables in a LAC, the LAC can be modified into another LAC using the method outlined above. The left-hand side of the LAC is modified and the right hand side remains the same. Simple algebraic manipulation is applied to normalize the LAC. I.e., to convert to a standard form xcexa3iaiwixe2x89xa6C or xcexa3iaiwi23 C. The modified LAC will typically have more variables then the original LAC, however, the ranges of the variables will be smaller. Further, there is no exponential increase in the number of variables or constraints; the total number of constraints and the total number of variables in the LAC will grow no more than the number of Boolean variables that are set to 0 or 1.
The above transformation is key to the seamless integration of Boolean clauses and LAC in this hybrid satisfiability algorithm. Next, there is described the satisfiability search which uses the above transformation, so word-level operators are expanded only when needed, resulting in greater efficiency.
If the LAC is empty, various special cases can be checked for in the 3-SAT clauses.
Essential variable: If a clause contains a single variable in true form (complemented form), clearly the variable has to be set to 1 (0) for the clause to be satisfied.
Dominating clause: If two clauses (ab) and (abc) exist, the latter clause can be deleted since the former implies the latter.
Unate variable: If a variable a appears only in true form, (complemented form) in all the clauses, the variable can immediately be set to 1 (0).
There are many other optimizations that could be applied for the 3-SAT problem.
In the general case, the LAC will be non-empty. Essential variables can still be checked for, and dominating clauses can be deleted. However, variables that are unate with respect to the Boolean clauses cannot be set without checking for correlation in the LAC. For example, given:
(w0ab)
W+Xxe2x89xa65
with w0 only appearing in the one clause shown, it""s still cannot be assumed that w0=1, because w0 is correlated with W. in order to satisfy the clauses and LAC, w0=0, a=1 might be needed.
The standard branching search is still performed to find a satisfying assignment. Only variables corresponding to inputs to the circuit will be set, and not intermediate signals (the intermediate signals may be set by implication on the clauses). First, special case pruning is performed, such as the checks mentioned above. There is a lot of structural information that can be exploited to simplify the 3-SAT clauses.
Regardless of correlation among bit-level and word-level variables, the following can be asserted:
Polynomial-time checks using cycle detection can be performed to see if 2-SAT+3-SAT is not feasible. If 2-SAT+3-SAT is infeasible, so it is HSAT. Note that, for 3-SAT, even if cycle detection fails, the problem may still be infeasible.
Full-fledged CNF satisfiability algorithms can be run with a limit on the number of back tracks in search, to possibly prove infeasibility of 3-SAT.
The linear program relaxation (LPR) of the LAC""s corresponds to relaxing the assumption that the word-level variables are integral (that is, they can be real). If the LPR corresponding to HSAT=2-SAT+3-SAT+LAC is infeasible, then the HSAT problem is infeasible.
If the problem is not infeasible, a Boolean variable or a word level variable is heuristically selected. If a Boolean variable is selected, it is set to 1, and the clauses and LAC""s are modified appropriately, and the satisfiability procedure is recursively called. If no satisfying assignment is found, the Boolean variable is then set to 0, the clauses and LAC""s are modified, and the satisfiability procedure is again recursively called. The selection of the variable is dependent on how many clauses and LAC""s it appears in. In the case of selecting a word-level variable, a check is made to see that no unknown Boolean variable correlated with that word-level variable exists (if so, another word-level variable or a Boolean variable is selected). The range of the word-level variable is split, and the two smaller ranges are used. The split is based on the value of the variable returned by the LPR. That is, if the word-level variable""s range is [xe2x88x927, 7], and the LPR returns a value of 4.5 for the variable, the procedure will recur on the [xe2x88x927, 4] and [5, 7] ranges. The only modification necessary, in this case, is to the LAC.
It is possible that LPR may return a feasible solution, but no integer solution may exist. If the LPR is feasible, and if the solution is integral and consistent across the word-level and bit-level variables, then there is a feasible solution to HSAT, and the procedure can stop.
When LPR returns a feasible, non-integral solution, a simple perturbation of the solution returned by LPR is performed to see if the solution can be made integral, while satisfying the consistency requirements. If so, there has been found a feasible solution to HSAT.
The CPU time allowed for search may be limited by limiting the number of back tracks. Given a certain number of back tracks, three things may happen:
1. An input assignment is found which produces the required output values.
2. It is determined that no input assignment satisfies the required values.
3. The certain number of back tracks may be exceeded before either of possibilities 1 or 2, mentioned above, occurs. In this case, the algorithm has failed to find a solution.
For example, consider the heavy path shown in FIG. 6. Assume it is desired to sensitize this path. There are three requirements:
Assuming unsigned numbers, to avoid underflow in the subtractor, it will be required that x greater than =y.
It will be required that c=1. This will translate to x greater than y when the module-input module-output relationships are included.
It will be required that d=0. This directly translates to rst=0.
Another example is depicted in FIG. 8, where LPR quickly detects infeasibility, but gate-level satisfiability typically requires a large number of back tracks to prove infeasibility. The bold path in the Fig. is FALSE, i.e., there is no assignment to the word-inputs X, Y, and Z that sensitizes it. One call to LPR will determine this. If gate-level satisfiability is used, the number of back tracks will depend on the order in which the bits of X, Y, and Z are assigned to O/I values. If the words are n bits wide, and the least significant bits are begun with, establishing infeasibility will require O(23n) back tracks. If the most significant bits of X, Y, and Z are set first, gate-level satisfiability will still require O(2n) back tracks, because infeasibility will not be detected for the cases of xi=yi=zi=0 and xi=yi=zi=1. It is possible that bits of word X or Y or Z appear in Boolean clauses due to additional circuitry. However, since correlation is taken into account during the search, appropriately modifying the LAC will allow the use of LPR and will outperform gate-level satisfiability.
If ordered Binary Decision Diagrams are used, under the right ordering, the BDD""s for the outputs of the comparators will grow linearly with bit-width. To determine infeasibility it is necessary to compute the intersection of the three BDD""s, and the time required for this will grow super-linearly with bit-width. Further, for more complex sets of (linear) arithmetic constraints, it is difficult to find an ordering (assuming one exists) that results in BDD""s of reasonable sizes.
Satisfiability problems generated during the justification step are similar to those generated in the path sensitization step. There are the module-input, module-output relationships, and additionally a requirement of particular values on register inputs.
The two primary reasons why the hybrid satisfiability algorithm may fail for a particular problem are nonlinear operations and large sequential depths. In this methodology, nonlinear operators have to be decomposed into linear arithmetic or Boolean operators. There are choices in the decomposition process. For example, it is possible to decompose nonlinear multiplication A*B into a large set of Boolean clauses. However, it is usually more efficient to transform this into linear constraints as described above.
Time-frame expansion works well for circuits with small sequential depths such as data paths, and small finite state machines. One case where time-frame expansion may become prohibitively expensive is when there are timers or counters in the circuit.
The first observability based approach relates to how to compute coverage given a set of predetermined input vectors. That is, the vectors must have already been selected prior to using the techniques described in the first observability based approach. The same may be said of the second observability based approach, which includes a more efficient way of computing the coverage for a set of input vectors that have already been selected. Neither of these two approaches describes how to generate vectors that, in the first instance, target the observability based coverage metric.
Previous efforts toward automated vector generation have not targeted the observability based coverage metric. For example, the article that describes the path coverage approach and the HSAT algorithm, described above for the purpose of explaining the HSAT algorithm, mentions how to automatically generate vectors but does not target the observability based coverage metric. Instead, this article describes automatic vector generation that targets a path coverage metric. In particular, it is a selective path coverage metric and not a complete path coverage metric.
The problem, then, in the VLSI design and verification field, is that there is no method for automatically generating vectors that target the observability based coverage metric. Such a method is needed.
It is therefore an object of the invention to solve the problem just mentioned.
More particularly, it is the object of this invention to provide a procedure for vector generation for observability-based statement coverage for HDL representations by combining vector generation with error simulation. The errors are modeled as tags. An HSAT procedure is used for vector generation.
In one embodiment, the object of the invention is realized in a method for vector generation which includes providing a representation of a design to be validated, automatically generating vectors that target the observability metric, and simulating errors (tags) for the representation. The simulation of errors includes modeling the errors as tags, and injecting the tags in the HDL code to determine the extent to which perturbations in a value at a location in the code will result in a value which is observable, i.e., propagates the error to an output or a register. In a preferred embodiment, the generation of the vector includes using a hybrid linear programming and Boolean satisfiability procedure. This procedure is also referred to as an HSAT procedure. The preferred embodiment also includes checking for tag coverage after each vector is generated, which may be referred to as repeated coverage computation.
To generate a vector, a tag list is prepared with each tag corresponding to one of the variable assignments in the HDL code 180. All the tags start out as uncovered, and then for each uncovered tag, the set of transitive fanout variables is marked and it is attempted to generate a vector that covers the uncovered tag by generating a set of linear and Boolean constraints, setting up an HSAT problem using those constraints, and finding a solution to the HSAT problem by solving the set of constraints. When such a vector can be generated, the tag is said to be covered by that vector, and an error occurring at the given location may be propagated to an observable output. After the vector is generated, tag simulation may be performed and any other tags covered by that same vector may be identified.
In the other preferred embodiments of the invention, different ways to help speed up the overall process are provided. For example, this includes randomly generating vectors and performing tag simulation with them, or generating constraints for only a limited number of paths at a time. In addition, the objective of the invention is also achieved in an especially preferred embodiment by maximizing the magnitude of the tags.
To put it another way, an important contribution of this invention is thus an automated vector generation procedure targeting the observability-based statement coverage metric. The invention, in one embodiment, provides for repeated coverage computation so as to minimize the number of generated vectors. The invention provides for various techniques to set up constraints based on the observability-based statement coverage metric. The constraints include interacting linear and Boolean constraints, and to solve this system of constraints, recent algorithms for solving HSAT problems are augmented. Various embodiments of the invention provide heuristics to control the number of constraints generated. In particular, the invention provides for the establishment and maintenance of a tag list during vector generation. Tags, which model the presence of an error, are associated with each variable assignment in the HDL code 180. After the generation of each vector, coverage by this vector of others of the tags in the HDL code 180 is determined using the efficient coverage computation procedure from the second approach to observability based coverage described above. Covered tags are deleted from or flagged in the tag list. The process is continued until all tags under the metric are covered, i.e. the tag list is empty, or until it is determined that the process will not generate a vector for a given tag within a predetermined period of time or within a predetermined level of computational effort.
The invention also involves a computer system, and computer program product for implementing the foregoing method. The invention, which will be explained with reference to various embodiments, will be better understood from the included figures which are provided merely for the sake of explanation, and are not intended to limit the invention.